\begin{tabbing}
$\forall$${\it MA}$:MsgA, $s$:${\it MA}$.state, $k$:Knd, $l$:IdLnk, ${\it vaal}$:${\it MA}$.V($k$), $i$:Id.
\\[0ex](source($l$) = $i$)
\\[0ex]$\Rightarrow$ \=${\it MA}$.send($k$;\+
\\[0ex]$l$;$s$;${\it vaal}$;map($\lambda$$x$.$x$.2;filter($\lambda$${\it ms}$.eqof(IdLnkDeq)(mlnk(${\it ms}$),$l$);${\it MA}$.sends($k$,$s$,${\it vaal}$)));$i$)
\-
\end{tabbing}